perm filename FRAC.LAN[EKL,SYS] blob
sn#860110 filedate 1988-08-17 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00010 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 (wipe-out)
C00005 00003 basic facts about factions new version
C00008 00004 ordering of fractions
C00014 00005 addition of fractions
C00019 00006 multiplication of fractions
C00025 00007 (proof pairing)
C00027 00008 (proof transfraction)
C00030 00009 more facts about ordering of fractions
C00035 00010 addition is welldefined
C00039 ENDMK
C⊗;
(wipe-out)
(get-proofs nat prf ekl sys)
(get-proofs lispax prf ekl sys)
(define cadr |cadr=λxv.car(cdr xv)|)
(define cddr |cddr=λxv.cdr(cdr xv)|)
;(ue (phi |λu.sexp car(u)|) listinduction)
(axiom |∀u.sexp car(u)|)
;∀U.LISTP CAR U
(label simpinfo)
;(ue (phi |λu.listp cdr(u)|) listinduction)
(axiom |∀u.listp cdr(u)|)
;∀U.LISTP CDR U
(label simpinfo)
(axiom |∀u.¬null cadr u ∧ null cddr u ⊃ list(car u, cadr u) = u|)
(label pairing)
;see proof below
(axiom |∀n.¬null(n)|)
(label simpinfo)
(axiom |∀n.sexp n|)
(label simpinfo)
;(trw |∀x y.car(list(x,y))=x| (use listdef mode: exact))
(axiom |∀x y.car(list(x,y))=x|)
;∀X Y.CAR LIST(X,Y)=X
(label simpinfo)
;(trw |∀x y.cadr(list(x,y))=y| (open cadr)(use listdef mode: always))
(axiom |∀x y.cadr(list(x,y))=y|)
;∀X Y.CADR(LIST(X,Y))=Y
(label simpinfo)
;basic facts about factions; new version
(proof fractions)
;Landau_def7
;definition of fractions as lists:
(decl (q q0 q1 q2 q3 q01 q02 q03) (type: |GROUND|) (sort: fr))
(axiom |∀q.listp q|)
(label simpinfo)
(axiom |∀q.null cddr q|)
(label fract0)(label simpinfo)
(axiom |∀m n.n≠0⊃fr(list(m,n))|)
(label fract1)(label simpinfo)
(axiom |∀q.natnum(car(q))∧natnum(cadr(q))∧cadr(q)≠0|)
(label fract2)(label simpinfo)
(label simpinfo nozerodivisors)
;(ue (u q) pairing)
(axiom |∀q.list(car q,cadr q)=q|)
;LIST(CAR Q,CADR(Q))=Q
(label fract4)(label simpinfo)
;Landau_def8
;equality among fractions
(decl ef (type: |@Q⊗@Q→TRUTHVAL|))
(define ef |ef=λq q0.if times(car(q),cadr(q0))=times(cadr(q),car(q0))
then true else false|)
(label efdef)
;(trw |fr(list(car q,cadr q))|)
(axiom |∀q.fr(list(car q,cadr q))|)
(label fract3)(label simpinfo)
;Landau_th37
;(trw |∀q.ef(q,q)| (open ef)(use commutmult))
(axiom |∀q.ef(q,q)|)
(label reflexf)
;Landau_th38
;(trw |∀q q0.ef(q,q0)⊃ef(q0,q)| (open ef)(part 1 (use commutmult)))
(axiom |∀q q0.ef(q,q0)⊃ef(q0,q)|)
(label symmf)
;Landau_th39
(axiom |∀q q1 q2.ef(q,q1)∧ef(q1,q2)⊃ef(q,q2)|)
(label transf)
;see proof below
;(trw |∀q q1 q2 q3.ef(q,q1)∧ef(q1,q2)∧ef(q2,q3)⊃ef(q,q3)|
; (use transf ue: ((q.q)(q1.q1)(q2.q2)) mode: exact)
; (use transf ue: ((q.q)(q1.q2)(q2.q3)) mode: exact))
(axiom |∀q q1 q2 q3.ef(q,q1)∧ef(q1,q2)∧ef(q2,q3)⊃ef(q,q3)|)
(label transf1)
;∀Q Q1 Q2 Q3.EF(Q,Q1)∧EF(Q1,Q2)∧EF(Q2,Q3)⊃EF(Q,Q3)
;Landau_th40
;(trw |∀q n.n≠0⊃ef(list(times(car q,n),times(cadr q,n)),q)| (open ef) commutmult
; (use listdef ltimescan mode: always))
;∀Q N.¬N=0⊃EF(LIST(CAR Q*N,CADR(Q)*N),Q)
(axiom |∀q n.n≠0⊃ef(list(times(car q,n),times(cadr q,n)),q)|)
(label fr_eqclass)
(show *)
;ordering of fractions
(proof frordering)
;Landau_def9
(decl gf (type: |@Q⊗@Q→TRUTHVAL|))
(define gf |gf=λq q0.if times(car(q),cadr(q0))>times(cadr(q),car(q0))
then true else false|)
;Landau_def10
(decl lf (type: |@Q⊗@Q→TRUTHVAL|))
(define lf |lf=λq q0.if times(car(q),cadr(q0))<times(cadr(q),car(q0))
then true else false|)
;Landau_th41
;(trw |∀q q0.lf(q,q0)∨ef(q,q0)∨gf(q,q0)|
; (open lf ef gf)(use commutmult totalord))
;∀Q Q0.LF(Q,Q0)∨EF(Q,Q0)∨GF(Q,Q0)
(axiom |∀q q0.lf(q,q0)∨ef(q,q0)∨gf(q,q0)|)
(label totalordfr)
;(trw |∀q q0.ef(q,q0)⊃¬lf(q,q0)∧¬gf(q,q0)| (open ef lf gf) strict1)
;∀Q Q0.EF(Q,Q0)⊃¬LF(Q,Q0)∧¬GF(Q,Q0)
(axiom |∀q q0.ef(q,q0)⊃¬lf(q,q0)∧¬gf(q,q0)|)
(label strictfr1)(label antisymless)(label strictlyless)
;(trw |∀q q0.gf(q,q0)⊃¬ef(q,q0)∧¬lf(q,q0)| (open ef lf gf) strict2)
;∀Q Q0.GF(Q,Q0)⊃¬EF(Q,Q0)∧¬LF(Q,Q0)
(axiom |∀q q0.gf(q,q0)⊃¬ef(q,q0)∧¬lf(q,q0)|)
(label strictfr2)
;(trw |∀q q0.lf(q,q0)⊃¬ef(q,q0)∧¬gf(q,q0)| (open ef lf gf) strict3)
;∀Q Q0.LF(Q,Q0)⊃¬EF(Q,Q0)∧¬GF(Q,Q0)
(axiom |∀q q0.lf(q,q0)⊃¬ef(q,q0)∧¬gf(q,q0)|)
(label strictfr3)
;Landau_th42 and 43
;(trw |∀q q0.gf(q,q0)≡lf(q0,q)| (open gf lf)
; (use greaterp_lessp commutmult))
;∀Q Q0.GF(Q,Q0)≡LF(Q0,Q)
(axiom |∀q q0.gf(q,q0)≡lf(q0,q)|)
(label simpinfo)(label gf_lf)
(axiom |∀q q1 q0.ef(q,q1)∧lf(q,q0)⊃lf(q1,q0)|)
(label ef_lf)
;see proof below
(axiom |∀q q0 q01.lf(q,q0)∧ef(q0,q01)⊃lf(q,q01)|)
(label lf_ef)
;exercise
;Landau_th44
;(trw |∀q q1 q0 q01.lf(q,q0)∧ef(q,q1)∧ef(q0,q01)⊃lf(q1,q01)|
; (use ef_lf ue: ((q.q)(q1.q1)(q0.q0)))(use lf_ef ue: ((q.q1)(q0.q0)(q01.q01))))
;∀Q Q1 Q0 Q01.LF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LF(Q1,Q01)
(axiom |∀q q1 q0 q01.lf(q,q0)∧ef(q,q1)∧ef(q0,q01)⊃lf(q1,q01)|)
(label lf_ef_ef_lf)
;Landau_th45
;(derive |∀q q1 q0 q01.gf(q,q0)∧ef(q,q1)∧ef(q0,q01)⊃gf(q1,q01)|
; * (use gf_lf mode: exact))
(axiom |∀q q1 q0 q01.gf(q,q0)∧ef(q,q1)∧ef(q0,q01)⊃gf(q1,q01)|)
(label gf_ef_ef_gf)
;Landau_def11
(decl gef (type: |@EF|))
(define gef |∀q q0.gef(q,q0)≡ef(q,q0)∨gf(q,q0)|)
(label gefdef)
;Landau_def12
(decl lef (type: |@EF|))
(define lef |∀q q0.lef(q,q0)≡ef(q,q0)∨lf(q,q0)|)
(label lefdef)
;Landau_th46
(axiom |∀q q1 q0 q01.gef(q,q0)∧ef(q,q1)∧ef(q0,q01)⊃gef(q1,q01)|)
(label Landau_th46)
;Landau_th47
(axiom |∀q q1 q0 q01.lef(q,q0)∧ef(q,q1)∧ef(q0,q01)⊃lef(q1,q01)|)
(label Landau_th47)
;Landau_th48 and 49
(axiom |∀q q0.gef(q,q0)≡lef(q0,q)|)
(label gef_lef)
;Landau_th50
(axiom |∀q1 q2 q3.lf(q1,q2)∧lf(q2,q3)⊃lf(q1,q3)|)
(label transordfr)
;see proof below
;Landau_a_th51
(axiom |∀q q1 q2.lef(q,q1)∧lf(q1,q2)⊃lf(q,q2)|)
(label Landau_a_th51)
;exercise
;Landau_b_th51
(axiom |∀q q1 q2.lf(q,q1)∧lef(q1,q2)⊃lf(q,q2)|)
(label Landau_b_th51)
;exercise
;Landau_th52
(axiom |∀q q1 q2.lef(q,q1)∧lef(q1,q2)⊃lef(q,q2)|)
(label Landau_th52)
;exercise
;Landau_th53
(axiom |∀q ∃q0.gf(q0,q)|)
(label nolastfr)
;exercise
;Landau_th54
(axiom |∀q ∃q0.lf(q0,q)|)
(label noleastfr)
;exercise (see file rational)
;Landau_th55
(axiom |∀q q1.∃q0.lf(q,q1)⊃lf(q,q0)∧lf(q0,q1)|)
(label densefr)
;exercise
;zero and one
(define qz |qz=list(0,1)|)
;(trw |fr qz| (open qz))
(axiom |fr qz|)
(label simpinfo)
(define qzerop |qzerop=λq.ef(q,qz)|)
(label qzeropdef)
;(derive |∀q.lef(qz,q)| zeroleast2 (open lef lf ef))
(axiom |∀q.lef(qz,q)|)
(label qzeroleast2)(label simpinfo)
(define qone |qone=list(1,1)|)
;QONE is unknown.
;the symbol QONE is given the same declaration as Q
;(trw |fr qone| (open qone))
(axiom |fr qone|)
(label simpinfo)
;FR(QONE)
;addition of fractions
(proof fractsum)
;Landau_def13
(decl pf (type: |@q⊗@q→@q|) (bindingpower: 940))
(define pf |pf=λq q0.list((car q*cadr q0)+(cadr q*car q0),(cadr q*cadr q0))|)
(label plusfdef)
;(trw |fr(pf(q,q0))| (open pf) fract1 nozerodivisors)
;FR(PF(Q,Q0))
(axiom |∀q q0.fr(pf(q,q0))|)
(label plusfsort)(label simpinfo)
;Landau_th56
(axiom |∀q q0 q1 q01.ef(q,q1)∧ef(q0,q01)⊃ef(pf(q,q0),pf(q1,q01))|)
(label sumf_uniqueness)
;see proof below
;Landau_th57
(axiom |∀q q0.cadr q=cadr q0⊃ef(pf(q,q0),list(car q+car q0,cadr q))|)
(label sumf_simpl)
;see proof below
;Landau_th58
;(trw |∀q q0.ef(pf(q,q0),pf(q0,q))|(open pf ef) (commutadd commutmult))
;∀Q Q0.EF(PF(Q,Q0),PF(Q0,Q))
(axiom |∀q q0.ef(pf(q,q0),pf(q0,q))|)
(label commutfadd)
;Landau_th59
;(trw |pf(pf(q,q0),q01)=pf(q,pf(q0,q01))| (open pf)(nuse commutmult commutadd)
; (use rdistrib ldistrib mode: exact))
;PF(PF(Q,Q0),Q01)=PF(Q,PF(Q0,Q01))
(axiom |∀q q0 q01.pf(pf(q,q0),q01)=pf(q,pf(q0,q01))|)
(label assocfadd)
;Landau_th60
(axiom |∀q q0.¬ef(q0,qz)⊃lf(q,pf(q,q0))|)
(label sumf_increasing)
;exercise
;Landau_th61 Landau_a_th62
(axiom |∀q q0 q01.lf(q,q0)⊃lf(pf(q,q01),pf(q0,q01))|)
(label lf_sumfpreserv)
;exercise
;Landau_b_th62
;(trw |∀q q0 q01.ef(q,q0)⊃ef(pf(q,q01),pf(q0,q01))|
; (use sumf_uniqueness ue: ((q.q)(q1.q0)(q0.q01)) ) reflexf)
;∀Q Q0 Q01.EF(Q,Q0)⊃EF(PF(Q,Q01),PF(Q0,Q01))
(axiom |∀q q0 q01.ef(q,q0)⊃ef(pf(q,q01),pf(q0,q01))| )
(label ef_sumfpreserv)
;Landau_c_th62
(axiom |∀q q0 q01.gf(q,q0)⊃gf(pf(q,q01),pf(q0,q01))|)
(label gf_sumfpreserv)
;exercise
;Landau_a_th63
(axiom |∀q q0 q01.gf(pf(q,q01),pf(q0,q01))⊃gf(q,q0)|)
(label gf_sumfsimpl)
;exercise
;Landau_b_th63
(axiom |∀q q0 q01.ef(pf(q,q01),pf(q0,q01))⊃ef(q,q0)|)
(label ef_sumfsimpl)
;exercise
;Landau_c_th63
(axiom |∀q q0 q01.lf(pf(q,q01),pf(q0,q01))⊃lf(q,q0)|)
(label lf_sumfsimpl)
;exercise
;Landau_th64
(axiom |∀q q0 q1 q01.gf(q,q0)∧gf(q1,q01)⊃gf(pf(q,q1),pf(q0,q01))|)
(label gf_gf_sumfpreserv)
;exercise
;Landau_a_th65
(axiom |∀q q0 q1 q01.lef(q,q0)∧lf(q1,q01)⊃lf(pf(q,q1),pf(q0,q01))|)
(label lef_lf_sumfpreserv)
;exercise
;Landau_b_th65
(axiom |∀q q0 q1 q01.lf(q,q0)∧lef(q1,q01)⊃lf(pf(q,q1),pf(q0,q01))|)
(label lf_lef_sumfpreserv)
;exercise
;Landau_th66
(axiom |∀q q0 q1 q01.lef(q,q0)∧lef(q1,q01)⊃lef(pf(q,q1),pf(q0,q01))|)
(label lef_lef_sumfpreserv)
;exercise
;(trw |∀q.ef(pf(q,qz),q)∧ef(pf(qz,q),q)|
; (open qz pf ef) commutmult)
;∀Q.EF(PF(Q,QZ),Q)∧EF(PF(QZ,Q),Q)
(axiom |∀q.ef(pf(q,qz),q)∧ef(pf(qz,q),q)|)
(label plus_qzero)(label simpinfo)
;Landau_th67
(axiom |∀q0 q.∃q1.lf(q,q0)⊃ef(pf(q,q1),q0)|)
(label minusdef)
;exercise
(define minus |∀q0 q.lf(q,q0)⊃ef(pf(q,minus(q0,q)),q0)| (minusdef choice))
(label minusdefinition)
(show *)
;multiplication of fractions
(proof fractmult)
(decl tf (type: |@Q⊗@Q→@Q|) (bindingpower: 935))
(define tf |tf=λq q0.list((car q*car q0),(cadr q*cadr q0))|)
(label timesfdef)
;(trw |∀q q0.fr(tf(q,q0))| (open tf))
;∀Q Q0.FR(TF(Q,Q0))
(axiom |∀q q0.fr(tf(q,q0))|)
(label simpinfo)
;Landau_th68
(axiom |∀q q0 q1 q01.ef(q,q1)∧ef(q0,q01)⊃ef(tf(q,q0),tf(q1,q01))|)
(label prodf_uniqueness)
;exercise
;Landau_th69
(axiom |∀q q0.ef(tf(q,q0),tf(q0,q))|)
(label commutfprod)
;exercise
;Landau_th70
(axiom |∀q q0 q01.tf(tf(q,q0),q01)=tf(q,tf(q0,q01))|)
(label assocfprod)
;exercise
;Landau_th71
(axiom |∀q q0 q01.tf(q,pf(q0,q01))=pf(tf(q,q0),tf(q,q01))|)
(label distribf_left)
;exercise
;Landau_a_th72
(axiom |∀q q1 q0.gf(q,q1)⊃gf(tf(q,q0),tf(q1,q0))|)
(label gf_prodfpreserv)
;exercise
;Landau_b_th72
(axiom |∀q q1 q0.ef(q,q1)⊃ef(tf(q,q0),tf(q1,q0))|)
(label ef_prodfpreserv)
;exercise
;Landau_c_th72
(axiom |∀q q1 q0.lf(q,q1)⊃lf(tf(q,q0),tf(q1,q0))|)
(label lf_prodfpreserv)
;exercise
;Landau_a_th73
(axiom |∀q q0 q01.gf(tf(q,q01),tf(q0,q01))⊃gf(q,q0)|)
(label gf_prodfsimpl)
;exercise
;Landau_b_th73
(axiom |∀q q0 q01.ef(tf(q,q01),tf(q0,q01))⊃ef(q,q0)|)
(label ef_prodfsimpl)
;exercise
;Landau_c_th73
(axiom |∀q q0 q01.lf(tf(q,q01),tf(q0,q01))⊃lf(q,q0)|)
(label lf_prodfsimpl)
;exercise
;Landau_th74
(axiom |∀q q1 q0 q01.gf(q,q1)∧gf(q0,q01)⊃gf(tf(q,q0),tf(q1,q01))|)
(label gf_gf_prodfpreserv)
;exercise
;Landau_a_th75
(axiom |∀q q1 q0 q01.lef(q,q1)∧lf(q0,q01)⊃lf(tf(q,q0),tf(q1,q01))|)
(label lef_lf_prodfpreserv)
;exercise
;Landau_b_th75
(axiom |∀q q1 q0 q01.lf(q,q1)∧lef(q0,q01)⊃lf(tf(q,q0),tf(q1,q01))|)
(label lf_lef_prodfpreserv)
;exercise
;Landau_th76
(axiom |∀q q1 q0 q01.lef(q,q1)∧lef(q0,q01)⊃lef(tf(q,q0),tf(q1,q01))|)
(label lef_lef_prodfpreserv)
;exercise
;the inverse of a fraction
(define inv |inv=λq.list(cadr q,car q)|)
(label invdef)
;(trw |∀q.¬qzerop q⊃fr(inv q)|
; (open qzerop qz ef inv)(use timesfacts mode: always))
;∀Q.¬QZEROP(Q)⊃FR(INV(Q))
(axiom |∀q.¬qzerop(q)⊃fr(inv(q))|)
(label simpinfo)(label invsort)
;times one
;(trw |∀q.tf(q,qone)=q| (open qone tf) (use timesfacts mode: exact)
; (use fract4 mode: always))
;∀Q.TF(Q,QONE)=Q
(axiom |∀q.tf(q,qone)=q|)
(label rtimes_qone)
;(trw |∀q.tf(qone,q)=q| (open qone tf) (use timesfacts mode: exact)
; (use fract4 mode: always))
;∀Q.TF(QONE,Q)=Q
(axiom |∀q.tf(qone,q)=q|)
(label ltimes_qone)
;(trw |∀q.¬qzerop q⊃ef(tf(q,inv(q)),qone)| (open inv tf qzerop qz qone ef)
; (use timesfacts mode: always)
; (use commutmult ue: ((n.|car q|)(m.|cadr q|)) mode: exact))
;∀Q.¬QZEROP(Q)⊃EF(TF(Q,INV(Q)),QONE)
(axiom |∀q.¬qzerop(q)⊃ef(tf(q,inv(q)),qone)|)
(label field)
;times zero
;(trw |∀q.ef(tf(q,qz),qz)| (open qz tf ef)
; (use timesfacts mode: always))
;∀Q.EF(TF(Q,QZ),QZ)
(axiom |∀q.ef(tf(q,qz),qz)|)
(label tfzf)
;Landau_a_th77
(axiom |∀q0 q.∃q1.¬qzerop q⊃ef(tf(q,q1),q0)|)
(label division)
;see proof below
(define divided |∀q q0.¬qzerop q⊃ef(tf(q,divided(q0,q)),q0)|
(division choice))
(label divisiondefinition)
(save-proofs frac)
(proof pairing)
(assume |cddr u = nil|)
(trw |car u.(cadr u.cddr u)| (use * mode: exact))
;CAR U.(CADR(U).CDDR(U))=CAR U.(CADR(U).NIL)
(trw |¬null u∧¬null cdr u⊃car u.(cadr(u).cddr u)=list (car u, cadr u)|
(use listdef mode: always) (use * mode: exact))
;¬NULL U∧¬NULL CDR U⊃CAR U.(CADR(U).CDDR(U))=LIST(CAR U,CADR(U))
(ci -3)
;CDDR(U)=NIL⊃(¬NULL U∧¬NULL CDR U⊃U=LIST(CAR U,CADR(U)))
;derive does not use all the information in simpinfo
(derive |∀u.null cddr(u)∧¬null u∧¬null cdr u⊃u=list(car u,cadr(u))| (* lispax#23))
(trw |null u∨null cdr(u)⊃ null cadr(u)| (open cadr) (use normal mode: exact))
;NULL U∨NULL CDR U⊃NULL CADR(U)
(derive |∀u.¬null cadr u ∧ null cddr u ⊃ list(car u, cadr u) = u| (-2 *))
(proof transfraction)
(assume |lf(q,q1) ∧ lf(q1,q2)|)
(label tf1)
(rw * (open lf))
;CAR Q*CADR(Q1)<CADR(Q)*CAR Q1∧CAR Q1*CADR(Q2)<CADR(Q1)*CAR Q2
(label tf2)
;deps: (TF1)
(assume |car q1 = 0|)
(label tf3)
(rw tf2 (use * zeroleast1 mode: exact) )
;FALSE
;deps: (TF1 TF3)
(ci tf3)
;¬CAR Q1=0
;deps: (TF1)
(trw |car q1 * cadr q1 ≠ 0| *)
;¬CAR Q1*CADR(Q1)=0
(label tf4)
;deps: (TF1)
;labels: LANDAU_TH34
;∀N M I J.N>M∧I>J⊃N*I>M*J
(ue ((n.|cadr q * car q1|)
(m.|car q * cadr q1|)
(i.|cadr q1 * car q2|)
(j.|car q1 * cadr q2|))
landau_th34 (use greaterp_lessp mode: always) tf2)
;CAR Q*CADR(Q1)*CAR Q1*CADR(Q2)<CADR(Q)*CAR Q1*CADR(Q1)*CAR Q2
;deps: (TF1)
(rw * (use commutmult))
;CAR Q*CAR Q1*CADR(Q1)*CADR(Q2)<CAR Q1*CAR Q2*CADR(Q)*CADR(Q1)
;deps: (TF1)
(trw |(car q * cadr q2) * (car q1 * cadr q1) <
(cadr q * car q2) * (car q1 * cadr q1)| * commutmult)
;(CAR Q*CADR(Q2))*(CAR Q1*CADR(Q1))<(CADR(Q)*CAR Q2)*(CAR Q1*CADR(Q1))
(label tf5)
;deps: (TF1)
;labels: LANDAU_C_TH33
;∀N M K.¬K=0∧M*K<N*K⊃M<N
(ue ((k.|car q1 * cadr q1|)
(m.|car q * cadr q2|)
(n.|cadr q * car q2|))
landau_c_th33 tf4 *)
;CAR Q*CADR(Q2)<CADR(Q)*CAR Q2
;deps: (TF1)
(trw |lf(q,q2)| * (open lf))
;LF(Q,Q2)
;deps: (TF1)
(ci tf1)
;LF(Q,Q1)∧LF(Q1,Q2)⊃LF(Q,Q2)
;more facts about ordering of fractions
(proof ef_lf)
(assume |ef(q,q1)∧lf(q,q0)|)
(label ef_lf1)
(rw * (open ef lf))
;CAR Q*CADR(Q1)=CADR(Q)*CAR Q1∧CAR Q*CADR(Q0)<CADR(Q)*CAR Q0
(label ef_lf2)
;deps: (EF_LF1)
;first case
(assume |car q=0|)
(label ef_lf3)
(rw ef_lf2 (use * mode: exact))
;0=CADR(Q)*CAR Q1∧0<CADR(Q)*CAR Q0
(label ef_lf4)
;deps: (EF_LF1 EF_LF3)
;labels: TIMESFACTS LTIMESTOZERO
;∀N K.¬N=0⊃N*K=0≡K=0
(ue ((n.|cadr q|)
(k.|car q1|))
ltimestozero *)
;CAR Q1=0
(label ef_lf5)
;deps: (EF_LF1 EF_LF3)
(assume |car q0=0|)
(label ef_lf6)
(rw ef_lf4 *)
;FALSE
;deps: (EF_LF1 EF_LF3 EF_LF6)
(ci ef_lf6)
;¬CAR Q0=0
(label ef_lf7)
;deps: (EF_LF1 EF_LF3)
;labels: SIMPINFO NOZERODIVISORS
;¬N=0∧¬M=0⊃¬N*M=0
(unlabel simpinfo nozerodivisors)
(ue ((n.|cadr q1|)
(m.|car q0|)) nozerodivisors *)
;¬CADR(Q1)*CAR Q0=0
;deps: (EF_LF1 EF_LF3)
(label simpinfo nozerodivisors)
(derive |0<cadr q1*car q0| (* zeroleast2))
(trw |lf(q1,q0)| (open lf) * ef_lf5)
;LF(Q1,Q0)
(label ef_lf8)
;deps: (EF_LF1 EF_LF3)
;second case
(assume |car q≠0|)
(label ef_lf9)
(trw |car q*cadr q1 ≠ 0| (* nozerodivisors))
;¬CAR Q*CADR(Q1)=0
(label ef_lf10)
;deps: (EF_LF9)
;labels: LANDAU_D_TH32
;∀N M K.N<M∧¬K=0⊃N*K<M*K
(ue ((k.|car q*cadr q1|)
(n.|car q*cadr q0|)
(m.|cadr q*car q0|))
landau_d_th32 ef_lf2 ef_lf10)
;CAR Q*CADR(Q0)*CAR Q*CADR(Q1)<CADR(Q)*CAR Q0*CAR Q*CADR(Q1)
;deps: (EF_LF1 EF_LF9)
(trw |(car q*cadr q0)*(cadr q*car q1)<cadr(q)*car q0*car q*cadr(q1)|
(use ef_lf2 mode: always direction: reverse) *)
;(CAR Q*CADR(Q0))*(CADR(Q)*CAR Q1)<CADR(Q)*CAR Q0*CAR Q*CADR(Q1)
;deps: (EF_LF1 EF_LF9)
(rw * commutmult)
;CAR Q*CAR Q1*CADR(Q)*CADR(Q0)<CAR Q*CAR Q0*CADR(Q)*CADR(Q1)
;deps: (EF_LF1 EF_LF9)
(trw |(car q1*cadr q0)*(car q*cadr q)<(cadr q1*car q0)*(car q*cadr q)|
(use commutmult) *)
;(CAR Q1*CADR(Q0))*(CAR Q*CADR(Q))<(CADR(Q1)*CAR Q0)*(CAR Q*CADR(Q))
(label ef_lf11)
;deps: (EF_LF1 EF_LF9)
(trw |car q*cadr q ≠ 0| ef_lf9 nozerodivisors)
;¬CAR Q*CADR(Q)=0
;deps: (EF_LF9)
;labels: LANDAU_C_TH33
;∀N M K.¬K=0∧M*K<N*K⊃M<N
(ue ((k.|car q*cadr q|)
(m.|car q1*cadr q0|)
(n.|cadr q1*car q0|))
landau_c_th33 * ef_lf11)
;CAR Q1*CADR(Q0)<CADR(Q1)*CAR Q0
;deps: (EF_LF1 EF_LF9)
(trw |lf(q1,q0)| (open lf) *)
;LF(Q1,Q0)
(label ef_lf12)
;deps: (EF_LF1 EF_LF9)
;conclude by cases
(trw |car q=0 ∨ car q≠0|)
;CAR Q=0∨¬CAR Q=0
(cases * ef_lf8 ef_lf12)
;LF(Q1,Q0)
;deps: (EF_LF1)
(ci ef_lf1)
;EF(Q,Q1)∧LF(Q,Q0)⊃LF(Q1,Q0)
;addition is welldefined
(proof sumf_uniqueness)
(assume |ef(q,q1)∧ef(q0,q01)|)
(label aw1)
(rw * (open ef) commutmult)
;CAR Q*CADR(Q1)=CAR Q1*CADR(Q)∧CAR Q0*CADR(Q01)=CAR Q01*CADR(Q0)
;deps: (AW1)
(trw |car q*cadr(q1)*cadr(q0)*cadr(q01)+car q0*cadr q01*cadr(q)*cadr(q1)=
car q1*cadr(q)*cadr(q0)*cadr(q01)+car q01*cadr(q0)*cadr(q)*cadr(q1)|
(use * mode: always))
;CAR Q*CADR(Q1)*CADR(Q0)*CADR(Q01)+CAR Q0*CADR(Q01)*CADR(Q)*CADR(Q1)=
;CAR Q1*CADR(Q)*CADR(Q0)*CADR(Q01)+CAR Q01*CADR(Q0)*CADR(Q)*CADR(Q1)
;deps: (AW1)
(rw * (use commutmult))
;CAR Q*CADR(Q1)*CADR(Q0)*CADR(Q01)+CAR Q0*CADR(Q)*CADR(Q1)*CADR(Q01)=
;CAR Q1*CADR(Q)*CADR(Q0)*CADR(Q01)+CAR Q01*CADR(Q)*CADR(Q1)*CADR(Q0)
;deps: (AW1)
(trw |ef(pf(q,q0),pf(q1,q01))| (open pf ef) (use rdistrib mode: always) commutmult *)
;EF(PF(Q,Q0),PF(Q1,Q01))
;deps: (AW1)
(ci aw1)
;EF(Q,Q1)∧EF(Q0,Q01)⊃EF(PF(Q,Q0),PF(Q1,Q01))